Iof proof for Lemma comp nat ind a:
1. P :
{k}
2.
i:. (j:. (j < i) 
P(j)) P(i)
3.
4. j :
5.
s:. (s < (j - 1)) P(s)
6. s :
7. s < j
P(s)
by ((% Establish desired induction hyp %
Assert
t:. (t < s) P(t))
ACollapseTHEN (IfLabL
ACol[`main`,OnHyps [7;5;4;3] Thin % cleanup %
AC;`assertion`,((((RepD)
ACollapseTHENM (InstHyp [t
AC] 5))
)
ACollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 3:n)) (first_tok :t
AC) inil_term)))
]))
AC1:
AC1: 3. s :
AC1: 4.
t:. (t < s) P(t)
AC1:
P(s)
AC.
T